Software product development is driven by two objectives: Short time-to-market and low development costs. Nevertheless, the current best practice of software development is time consuming, and creates unnecessary expense. It is frequently only in the later stages of product development, or even after product deployment, that additional expense visible. For instance because software bugs remain in the code, and only come to light after the software is in use. Such bugs are time consuming to detect. Finding software bugs, and providing assurance of their absence, is therefore of great importance in software development.
In contrast to equation solving approaches to static analysis, an ‘automata based’ approach defines properties in terms of temporal logic expressions over annotated graphs, see references [4, 2, 6]. The validity of a property can then be checked automatically by graph exploring techniques such as model checking, see references [1, 5].
The basic approach is to map a C/C++ program to its corresponding control flow graph (CFG), and to label the CFG with occurrences of syntactic constructs of interest; such as those that pass pointers of variables. The CFG together with the labels are then mapped to the input language of a model checker or directly translated into a Kripke structure for model checking, A Kripke structure is a set of labeled states, equipped with a (total) transition relation. This framework can be applied to the analysis of individual functions of a C/C++ program.